E, X1, X2:Type, info:(E(IdX1+(IdLnkE)X2)), pred?:(E(E+Unit)),
p:(e:E, l:IdLnk.
p:(e':E.
p:(e'':E.
p:(rcv?(e'')
p:( sender(e'') = e
p:( link(e'') = l
p:( e'' = e'  e'' < e' & loc(e') = destination(l)  Id), r:E.
SWellFounded(pred!(e;e'))
 (e:E. first(e)  loc(pred(e)) = loc(e)  Id)
 (e, e':E. loc(e) = loc(e')  Id  pred?(e) = pred?(e')  e = e')
 rcv?(r)
 (r ((x,y. first(y) & x = pred(y)  E)^*) sends-bound(p;sender(r);link(r))) 

latex

Definitions	ecase1(e;info;i.f(i);l,e'.g(l;e')), True, sends-bound(p;e;l), R^+, A & B, sender(e), link(e), first(e), pred(e), SWellFounded(R(x;y)), x,y. t(x;y), pred!(e;e'), x:A. B(x), b, rcv?(e), e < e', Prop, loc(e), destination(l), Unit, Id, IdLnk, {T}, t  T, P & Q, x:A. B(x), A, False, P  Q, x f y, R^*, P  Q
Lemmas	link wf, sender wf, sends-bound-property, IdLnk wf, Id wf, unit wf, ldst wf, loc wf, cless wf, rcv? wf, assert wf, pred! wf, strongwellfounded wf, pred wf, first wf, not wf, rel star weakening, cless-eq-loc, sends-bound wf, rel-plus-rel-star, true wf, false wf